A, B, C:Type, g:(A(B + Top)), f:(B(C + Top)), x:A.
can-apply(f o g  ;x) ~ (can-apply(g;x)  can-apply(f;do-apply(g;x))) 

latex

ProofTree

Definitions

left + right, t  T, x:AB(x), P  Q, x:A. B(x), s = t, Top, f(a), do-apply(f;x), can-apply(f;x), f o g  , Type